T:Type, L:((T) List), P:(T).
(x:T. Dec(P(x)))
 (QL. x:T. Dec(Q(x)))
 (QL. finite-type({x:T| Q(x)} ))
 (x:T. P(x)  (QL.Q(x)))
 finite-type({x:T| P(x)} ) 

latex

Definitions	x:A. B(x), , P  Q, x(s), t  T, x. t(x), A  B, A, False, x:A. B(x), Top, S  T, P  Q, P & Q, P  Q, {i..j}, i  j < k, (x  l), A c B, , SQType(T), {T}, T, True, t.1, xL. P(x), (xL.P(x))
Lemmas	finite-decidable-set, l exists wf, l all wf2, finite-type wf, l member wf, decidable wf, select wf, select member, int seg wf, length wf1, concat wf, map wf, pi1 wf, upto wf, length wf nat, top wf, member-concat, exists functionality wrt iff, and functionality wrt iff, member map, le wf, member upto